 | ||||||
 |
 |
 |
 |
 |
 |
 |
 | ||||||
 |
 | |||||
|
|
|
|
| WEDNESDAY, June 9, 2004, 4:30 PM - 6:30 PM | Room: 6A | ||
|
TOPIC AREA: SYSTEM-LEVEL DESIGN AND VERIFICATION | ||
| SESSION 31 | |||
| Advances in Boolean Analysis Techniques | |||
| Chair: Aarti Gupta - NEC Corp., Princeton, NJ | |||
| Organizers: Pei-Hsin Ho, Tony Ma | |||
| Recent years have witnessed significant advances in the scalability and applicability of Boolean reasoning methods in a variety of EDA problems. Papers in this session represent significant extensions to the state-of-the-art technology in this area. The first paper proposes a SAT-based method for diagnosing infeasibility. The second paper uses re-parametrization to improve symbolic simulation. The third paper presents efficient symmetry detection methods. The last two papers describe methods for enhancing bounded model checking and combinational equivalence checking. | |||
 31.1 |
AMUSE: A Minimally-Unsatisfiable Subformula Extractor |
||
| Speaker(s): | Maher N. Mneimneh - Univ. of Michigan, Ann Arbor, MI | ||
| Author(s): | Yoonna Oh - Univ. of Michigan, Ann Arbor, MI Maher N. Mneimneh - Univ. of Michigan, Ann Arbor, MI Zaher S. Andraus - Univ. of Michigan, Ann Arbor, MI Karem A. Sakallah - Univ. of Michigan, Ann Arbor, MI Igor L. Markov - Univ. of Michigan, Ann Arbor, MI | ||
| 31.2 | A SAT-Based Algorithm for Reparameterization in Symbolic Simulation | ||
| Speaker(s): | Pankaj P. Chauhan - Carnegie Mellon Univ., Pittsburgh, PA | ||
| Author(s): | Pankaj P. Chauhan - Carnegie Mellon Univ., Pittsburgh, PA Edmund M. Clarke - Carnegie Mellon Univ., Pittsburgh, PA Daniel Kroening - Carnegie Mellon Univ., Pittsburgh, PA | ||
| 31.3 | Exploiting Structure in Symmetry Detection for CNF | ||
| Speaker(s): | Paul T. Darga - Univ. of Michigan, Ann Arbor, MI | ||
| Author(s): | Paul T. Darga - Univ. of Michigan, Ann Arbor, MI Mark H. Liffiton - Univ. of Michigan, Ann Arbor, MI Karem A. Sakallah - Univ. of Michigan, Ann Arbor, MI Igor L. Markov - Univ. of Michigan, Ann Arbor, MI | ||
| 31.4s | Refining the SAT Decision Ordering for Bounded Model Checking | ||
| Speaker(s): | Chao Wang - Univ. of Colorado, Boulder, CO | ||
| Author(s): | Chao Wang - Univ. of Colorado, Boulder, CO HoonSang Jin - Univ. of Colorado, Boulder, CO Gary D. Hachtel - Univ. of Colorado, Boulder, CO Fabio Somenzi - Univ. of Colorado, Boulder, CO | ||
| 31.5s | Efficient Equivalence Checking with Partitions and Hierarchical Cut-Points | ||
| Speaker(s): | Lisa R. McIlwain - Synopsys, Inc., Hillsboro, OR | ||
| Author(s): | Demosthenes Anastasakis - Synopsys, Inc., Hillsboro, OR Lisa R. Mcilwain - Synopsys, Inc., Hillsboro, OR Slawomir Pilarski - Univ. of Washington, Tacoma, WA | ||
 | |||